_ ← defineName p.name (.parameter p) (some $ dt.name.text ++ ".." ++ p.name.text ++ "!")

-- Before:
  recurse (expr : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := do
    let md := expr.md
    match _h : expr.val with
    ...
    termination_by sizeOf expr
    decreasing_by
      all_goals (simp_wf; try term_by_mem)
      ...

-- After:
  recurse (exprMd : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := do
    let ⟨expr, md⟩ := exprMd
    match _h : expr with
    ...
    termination_by sizeOf exprMd

  recurse (exprMd : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := do
    let ⟨expr, md⟩ := exprMd
    match _h : expr with
    | .FieldSelect selectTarget fieldName =>
        let qualifiedName : Identifier := resolveQualifiedFieldName model fieldName
        let valTy := (model.get fieldName).getType.getD (panic! "heapTransformExpr1")
        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Identifier heapVar), selectTarget, mkMd (.StaticCall qualifiedName [])], md ⟩
        -- Unwrap Box: apply the appropriate destructor
        return mkMd <| .StaticCall (boxDestructorName valTy.val) [readExpr]
    | .StaticCall callee args =>
        let args' ← args.attach.mapM (fun ⟨v, _⟩ => recurse v)
        let calleeReadsHeap ← readsHeap callee
        let calleeWritesHeap ← writesHeap callee
        if calleeWritesHeap then
          if valueUsed then
            let freshVar ← freshVarName
            let varDecl := mkMd (.LocalVariable freshVar ⟨.TInt, #[]⟩ none)
            let callWithHeap := ⟨ .Assign
              [mkMd (.Identifier heapVar), mkMd (.Identifier freshVar)]
              (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), md ⟩), md ⟩
            return ⟨ .Block [varDecl, callWithHeap, mkMd (.Identifier freshVar)] none, md ⟩
          else
            return ⟨ .Assign [mkMd (.Identifier heapVar)] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), md ⟩), md ⟩
        else if calleeReadsHeap then
          return ⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), md ⟩
        else
          return ⟨ .StaticCall callee args', md ⟩
    | .InstanceCall callTarget callee args =>
        let t ← recurse callTarget
        let args' ← args.mapM (recurse ·)
        return ⟨ .InstanceCall t callee args', md ⟩
    | .IfThenElse c t e =>
        let e' ← match e with | some x => some <$> recurse x valueUsed | none => pure none
        return ⟨ .IfThenElse (← recurse c) (← recurse t valueUsed) e', md ⟩
    | .Block stmts label =>
        let n := stmts.length
        let rec processStmts (idx : Nat) (remaining : List StmtExprMd) : TransformM (List StmtExprMd) := do
          match remaining with
          | [] => pure []
          | s :: rest =>
              let isLast := idx == n - 1
              let s' ← recurse s (isLast && valueUsed)
              let rest' ← processStmts (idx + 1) rest
              pure (s' :: rest')
          termination_by sizeOf remaining
        let stmts' ← processStmts 0 stmts
        return ⟨ .Block stmts' label, md ⟩
    | .LocalVariable n ty i =>
        let i' ← match i with | some x => some <$> recurse x | none => pure none
        return ⟨ .LocalVariable n ty i', md ⟩
    | .While c invs d b =>
        let invs' ← invs.mapM (recurse ·)
        return ⟨ .While (← recurse c) invs' d (← recurse b false), md ⟩
    | .Return v =>
        let v' ← match v with | some x => some <$> recurse x | none => pure none
        return ⟨ .Return v', md ⟩
    | .Assign targets v =>
        match targets with
        | [⟨.FieldSelect target fieldName, _fieldSelectMd⟩] =>
          let qualifiedName : Identifier := resolveQualifiedFieldName model fieldName
          let valTy := (model.get fieldName).getType.getD (panic! "heapTransformExpr2")
          let target' ← recurse target
          let v' ← recurse v
          -- Wrap value in Box constructor
          let boxedVal := mkMd <| .StaticCall (boxConstructorName valTy.val) [v']
          let heapAssign := ⟨ .Assign [mkMd (.Identifier heapVar)]
            (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), md ⟩
          if valueUsed then
            return ⟨ .Block [heapAssign, v'] none, md ⟩
          else
            return heapAssign
        | fields =>
            let targets' ← fields.mapM (recurse ·)
            return ⟨ .Assign targets' (← recurse v), md ⟩
    | .PureFieldUpdate t f v => return ⟨ .PureFieldUpdate (← recurse t) f (← recurse v), md ⟩
    | .PrimitiveOp op args =>
      let args' ← args.mapM (recurse ·)
      -- For == and != on Composite types, compare refs instead
      match op, args with
      | .Eq, [e1, _e2] =>
        let ty := (computeExprType model e1).val
        match ty with
        | .UserDefined _ =>
          let ref1 := mkMd (.StaticCall "Composite..ref!" [args'[0]!])
          let ref2 := mkMd (.StaticCall "Composite..ref!" [args'[1]!])
          return ⟨ .PrimitiveOp .Eq [ref1, ref2], md ⟩
        | _ => return ⟨ .PrimitiveOp op args', md ⟩
      | .Neq, [e1, _e2] =>
        let ty := (computeExprType model e1).val
        match ty with
        | .UserDefined _ =>
          let ref1 := mkMd (.StaticCall "Composite..ref!" [args'[0]!])
          let ref2 := mkMd (.StaticCall "Composite..ref!" [args'[1]!])
          return ⟨ .PrimitiveOp .Neq [ref1, ref2], md ⟩
        | _ => return ⟨ .PrimitiveOp op args', md ⟩
      | _, _ => return ⟨ .PrimitiveOp op args', md ⟩
    | .New _ => return exprMd
    | .ReferenceEquals l r => return ⟨ .ReferenceEquals (← recurse l) (← recurse r), md ⟩
    | .AsType t ty =>
        let t' ← recurse t valueUsed
        let isCheck := ⟨ .IsType t' ty, md ⟩
        let assertStmt := ⟨ .Assert isCheck, md ⟩
        return ⟨ .Block [assertStmt, t'] none, md ⟩
    | .IsType t ty => return ⟨ .IsType (← recurse t) ty, md ⟩
    | .Forall p trigger b =>
        let trigger' ← trigger.attach.mapM fun ⟨t, _⟩ => recurse t
        return ⟨ .Forall p trigger' (← recurse b), md ⟩
    | .Exists p trigger b =>
        let trigger' ← trigger.attach.mapM fun ⟨t, _⟩ => recurse t
        return ⟨ .Exists p trigger' (← recurse b), md ⟩
    | .Assigned n => return ⟨ .Assigned (← recurse n), md ⟩
    | .Old v => return ⟨ .Old (← recurse v), md ⟩
    | .Fresh v => return ⟨ .Fresh (← recurse v), md ⟩
    | .Assert c => return ⟨ .Assert (← recurse c), md ⟩
    | .Assume c => return ⟨ .Assume (← recurse c), md ⟩
    | .ProveBy v p => return ⟨ .ProveBy (← recurse v) (← recurse p), md ⟩
    | .ContractOf ty f => return ⟨ .ContractOf ty (← recurse f), md ⟩
    | _ => return exprMd
    termination_by sizeOf exprMd

// This test fails because Core incorrectly report error locations on procedure preconditions
// procedure multipleRequiresCaller() {
//  var a: int := multipleRequires(1, 2);
//  var b: int := multipleRequires(-1, 2);
// error: assertion does not hold
// }